{-# 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.Conway.Base (
  externalFunctions,
) where

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

-- ======================================================================

externalFunctions :: Agda.ExternalFunctions
externalFunctions :: ExternalFunctions
externalFunctions = Agda.MkExternalFunctions {Integer -> Integer -> Integer -> Bool
extIsSigned :: Integer -> Integer -> Integer -> 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 Any -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
            (VKey Any -> VerKeyDSIGN DSIGN)
-> (Maybe (VKey Any) -> VKey Any)
-> Maybe (VKey Any)
-> VerKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey Any -> Maybe (VKey Any) -> VKey Any
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> VKey Any
forall a. HasCallStack => [Char] -> a
error [Char]
"Failed to convert an Agda VKey to a Haskell VKey")
            (Maybe (VKey Any) -> VerKeyDSIGN DSIGN)
-> Maybe (VKey Any) -> VerKeyDSIGN DSIGN
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe (VKey Any)
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