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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Base (
  externalFunctions,
) where

import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
import Cardano.Ledger.Core (HASH, Hash)
import Cardano.Ledger.Keys (DSIGN, VKey (..))
import Data.ByteString (ByteString)
import Data.Either (isRight)
import Data.Maybe (fromMaybe)
import qualified MAlonzo.Code.Ledger.Core.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (signatureFromInteger, vkeyFromInteger)
import Test.Cardano.Ledger.Conformance.Utils (integerToHash)

externalFunctions :: Agda.ExternalFunctions
externalFunctions :: ExternalFunctions
externalFunctions = Agda.MkExternalFunctions {Bool
Integer -> Integer -> Integer -> Bool
extIsSigned :: Integer -> Integer -> Integer -> Bool
extValidPlutusScript :: Bool
extValidPlutusScript :: Bool
extIsSigned :: Integer -> Integer -> Integer -> Bool
..}
  where
    extIsSigned :: Integer -> Integer -> Integer -> Bool
extIsSigned Integer
vk Integer
ser Integer
sig =
      Either [Char] () -> Bool
forall a b. Either a b -> Bool
isRight (Either [Char] () -> Bool) -> Either [Char] () -> Bool
forall a b. (a -> b) -> a -> b
$
        forall v a.
(DSIGNAlgorithm v, Signable v a, HasCallStack) =>
ContextDSIGN v
-> VerKeyDSIGN v -> a -> SignedDSIGN v a -> Either [Char] ()
verifySignedDSIGN
          @DSIGN
          @(Hash HASH ByteString)
          ()
          VerKeyDSIGN DSIGN
vkey
          Hash HASH ByteString
hash
          SignedDSIGN DSIGN (Hash HASH ByteString)
signature
      where
        vkey :: VerKeyDSIGN DSIGN
vkey =
          VKey (ZonkAny 0) -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
            (VKey (ZonkAny 0) -> VerKeyDSIGN DSIGN)
-> (Maybe (VKey (ZonkAny 0)) -> VKey (ZonkAny 0))
-> Maybe (VKey (ZonkAny 0))
-> VerKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey (ZonkAny 0) -> Maybe (VKey (ZonkAny 0)) -> VKey (ZonkAny 0)
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> VKey (ZonkAny 0)
forall a. HasCallStack => [Char] -> a
error [Char]
"Failed to convert an Agda VKey to a Haskell VKey")
            (Maybe (VKey (ZonkAny 0)) -> VerKeyDSIGN DSIGN)
-> Maybe (VKey (ZonkAny 0)) -> VerKeyDSIGN DSIGN
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (VKey (ZonkAny 0))
forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger Integer
vk
        hash :: Hash HASH ByteString
hash =
          Hash HASH ByteString
-> Maybe (Hash HASH ByteString) -> Hash HASH ByteString
forall a. a -> Maybe a -> a
fromMaybe
            ([Char] -> Hash HASH ByteString
forall a. HasCallStack => [Char] -> a
error ([Char] -> Hash HASH ByteString) -> [Char] -> Hash HASH ByteString
forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to get hash from integer:\n" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
ser)
            (Maybe (Hash HASH ByteString) -> Hash HASH ByteString)
-> Maybe (Hash HASH ByteString) -> Hash HASH ByteString
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (Hash HASH ByteString)
forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
integerToHash Integer
ser
        signature :: SignedDSIGN DSIGN (Hash HASH ByteString)
signature =
          SigDSIGN DSIGN -> SignedDSIGN DSIGN (Hash HASH ByteString)
forall v a. SigDSIGN v -> SignedDSIGN v a
SignedDSIGN
            (SigDSIGN DSIGN -> SignedDSIGN DSIGN (Hash HASH ByteString))
-> (Maybe (SigDSIGN DSIGN) -> SigDSIGN DSIGN)
-> Maybe (SigDSIGN DSIGN)
-> SignedDSIGN DSIGN (Hash HASH ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDSIGN DSIGN -> Maybe (SigDSIGN DSIGN) -> SigDSIGN DSIGN
forall a. a -> Maybe a -> a
fromMaybe
              ([Char] -> SigDSIGN DSIGN
forall a. HasCallStack => [Char] -> a
error [Char]
"Failed to decode the signature")
            (Maybe (SigDSIGN DSIGN)
 -> SignedDSIGN DSIGN (Hash HASH ByteString))
-> Maybe (SigDSIGN DSIGN)
-> SignedDSIGN DSIGN (Hash HASH ByteString)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (SigDSIGN DSIGN)
forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger Integer
sig

    extValidPlutusScript :: Bool
extValidPlutusScript = Bool
True