{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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,
  DataHash,
  Era,
  Hash,
  KeyHash (..),
  KeyRole (..),
  PParams (..),
  PParamsHKD,
  PParamsUpdate (..),
  SafeHash,
  ScriptHash (..),
  TxAuxDataHash (..),
  extractHash,
  hashAnnotated,
 )
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.CostModels (CostModels, costModelsValid)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.Plutus.ExUnits (ExUnits (..), Prices)
import Cardano.Ledger.Plutus.Language (Language (..))
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Control.Monad (forM)
import Control.Monad.Except (throwError)
import Data.Functor.Identity (Identity (..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe.Strict (StrictMaybe (..))
import GHC.Natural (naturalToInteger)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
 )
import Test.Cardano.Ledger.Conformance.Utils

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 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 (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 SpecTranslate ctx StakeReference where
  type SpecRep StakeReference = Maybe Agda.Credential

  toSpecRep :: StakeReference -> SpecTransM ctx (SpecRep StakeReference)
toSpecRep (StakeRefBase Credential Staking
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
<$> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
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
_ = Text -> SpecTransM ctx BootstrapAddr
forall a. Text -> SpecTransM ctx a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Text
"Cannot translate bootstrap addresses"

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

  toSpecRep :: Addr -> SpecTransM ctx (SpecRep 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 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
<*> Credential Payment -> SpecTransM ctx (SpecRep (Credential Payment))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Payment
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 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 (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

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

deriving instance SpecTranslate ctx Coin

deriving instance SpecTranslate ctx SlotNo

deriving instance SpecTranslate ctx EpochNo

deriving instance SpecTranslate ctx EpochInterval

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

  toSpecRep :: ProtVer -> SpecTransM ctx (SpecRep ProtVer)
toSpecRep (ProtVer Version
ver Natural
minor) = (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, Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
minor)

instance SpecTranslate ctx Language where
  type SpecRep Language = Agda.HSLanguage

  toSpecRep :: Language -> SpecTransM ctx (SpecRep Language)
toSpecRep Language
l = case Language
l of
    Language
PlutusV1 -> HSLanguage -> SpecTransM ctx HSLanguage
forall a. a -> SpecTransM ctx a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV1
    Language
PlutusV2 -> HSLanguage -> SpecTransM ctx HSLanguage
forall a. a -> SpecTransM ctx a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV2
    Language
PlutusV3 -> HSLanguage -> SpecTransM ctx HSLanguage
forall a. a -> SpecTransM ctx a
forall (m :: * -> *) a. Monad m => a -> m a
return HSLanguage
Agda.PV3
    Language
PlutusV4 -> String -> SpecTransM ctx HSLanguage
forall a. HasCallStack => String -> a
error String
"PlutusV4 not supported"

instance SpecTranslate ctx CostModels where
  type SpecRep CostModels = Agda.LanguageCostModels

  toSpecRep :: CostModels -> SpecTransM ctx (SpecRep CostModels)
toSpecRep CostModels
cm =
    -- filter out PlutusV4 language
    let validCostModels :: [(Language, CostModel)]
validCostModels = ((Language, CostModel) -> Bool)
-> [(Language, CostModel)] -> [(Language, CostModel)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Language -> Language -> Bool
forall a. Eq a => a -> a -> Bool
/= Language
PlutusV4) (Language -> Bool)
-> ((Language, CostModel) -> Language)
-> (Language, CostModel)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Language, CostModel) -> Language
forall a b. (a, b) -> a
fst) ([(Language, CostModel)] -> [(Language, CostModel)])
-> [(Language, CostModel)] -> [(Language, CostModel)]
forall a b. (a -> b) -> a -> b
$ Map Language CostModel -> [(Language, CostModel)]
forall k a. Map k a -> [(k, a)]
Map.toList (CostModels -> Map Language CostModel
costModelsValid CostModels
cm)
     in [(HSLanguage, ())] -> LanguageCostModels
Agda.MkLanguageCostModels ([(HSLanguage, ())] -> LanguageCostModels)
-> SpecTransM ctx [(HSLanguage, ())]
-> SpecTransM ctx LanguageCostModels
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Language, CostModel) -> SpecTransM ctx (HSLanguage, ()))
-> [(Language, CostModel)] -> SpecTransM ctx [(HSLanguage, ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Language
l, CostModel
_) -> (,()) (HSLanguage -> (HSLanguage, ()))
-> SpecTransM ctx HSLanguage -> SpecTransM ctx (HSLanguage, ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Language -> SpecTransM ctx (SpecRep Language)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Language
l) [(Language, CostModel)]
validCostModels

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 Natural
a Natural
b) = (Integer, Integer) -> SpecTransM ctx (Integer, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
a, Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
b)

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

  toSpecRep :: AccountAddress -> SpecTransM ctx (SpecRep AccountAddress)
toSpecRep (AccountAddress Network
n (AccountId Credential Staking
c)) = Integer -> Credential -> RewardAddress
Agda.RewardAddress (Integer -> Credential -> RewardAddress)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> RewardAddress)
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 -> RewardAddress)
-> SpecTransM ctx Credential -> SpecTransM ctx RewardAddress
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
c

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 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
  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 (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

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 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
    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)
    pure Agda.MkHSVKey {..}

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 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

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

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 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 (SpecRep (KeyHash StakePool)) Agda.Coin

  toSpecRep :: PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
toSpecRep (PoolDistr Map (KeyHash StakePool) IndividualPoolStake
ps NonZero Coin
_) = 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

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

  toSpecRep :: BlocksMade -> SpecTransM ctx (SpecRep BlocksMade)
toSpecRep (BlocksMade Map (KeyHash StakePool) Natural
m) = do
    xs <- [(KeyHash StakePool, Natural)]
-> ((KeyHash StakePool, Natural)
    -> SpecTransM ctx (Integer, Integer))
-> SpecTransM ctx [(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 ctx (Integer, Integer))
 -> SpecTransM ctx [(Integer, Integer)])
-> ((KeyHash StakePool, Natural)
    -> SpecTransM ctx (Integer, Integer))
-> SpecTransM ctx [(Integer, Integer)]
forall a b. (a -> b) -> a -> b
$ \(KeyHash StakePool
k, Natural
v) -> do
      k' <- KeyHash StakePool -> SpecTransM ctx (SpecRep (KeyHash StakePool))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash StakePool
k
      pure (k', naturalToInteger v)
    pure $ Agda.MkHSMap xs