{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# 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 (Addr (..), BootstrapAddress (..), RewardAccount (..))
import Cardano.Ledger.BaseTypes (
  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)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.Plutus.ExUnits (ExUnits (..), Prices)
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Control.Monad.Except (throwError)
import Data.Functor.Identity (Identity (..))
import Data.Map (Map)
import Data.Maybe.Strict (StrictMaybe (..))
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 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
_ = 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 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 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 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 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 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
  ( 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
    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 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 CompactForm 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