{-# 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 (
  BLS12381MinSigDSIGN,
  PossessionProofDSIGN,
  SignedDSIGN (..),
  VerKeyDSIGN,
  verifyPossessionProofDSIGN,
  verifySignedDSIGN,
 )
import Cardano.Crypto.DSIGN.BLS12381.Internal (minSigPoPDST)
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 (
  popFromInteger,
  signatureFromInteger,
  verkeyFromInteger96,
  vkeyFromInteger,
 )
import Test.Cardano.Ledger.Conformance.Utils (integerToHash)

externalFunctions :: Agda.ExternalFunctions
externalFunctions :: ExternalFunctions
externalFunctions = Agda.MkExternalFunctions {Bool
Integer -> Integer -> Bool
Integer -> Integer -> Integer -> Bool
extIsSigned :: Integer -> Integer -> Integer -> Bool
extIsValidPoP :: Integer -> Integer -> Bool
extValidPlutusScript :: Bool
extValidPlutusScript :: Bool
extIsValidPoP :: 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 (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

    extIsValidPoP :: Integer -> Integer -> Bool
extIsValidPoP Integer
vk Integer
pop =
      Either [Char] () -> Bool
forall a b. Either a b -> Bool
isRight (Either [Char] () -> Bool) -> Either [Char] () -> Bool
forall a b. (a -> b) -> a -> b
$
        ContextDSIGN BLS12381MinSigDSIGN
-> VerKeyDSIGN BLS12381MinSigDSIGN
-> PossessionProofDSIGN BLS12381MinSigDSIGN
-> Either [Char] ()
forall v.
(DSIGNAggregatable v, HasCallStack) =>
ContextDSIGN v
-> VerKeyDSIGN v -> PossessionProofDSIGN v -> Either [Char] ()
verifyPossessionProofDSIGN ContextDSIGN BLS12381MinSigDSIGN
BLS12381SignContext
minSigPoPDST VerKeyDSIGN BLS12381MinSigDSIGN
verkey PossessionProofDSIGN BLS12381MinSigDSIGN
proofofpossesion
      where
        verkey :: VerKeyDSIGN BLS12381MinSigDSIGN
        verkey :: VerKeyDSIGN BLS12381MinSigDSIGN
verkey =
          VerKeyDSIGN BLS12381MinSigDSIGN
-> Maybe (VerKeyDSIGN BLS12381MinSigDSIGN)
-> VerKeyDSIGN BLS12381MinSigDSIGN
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> VerKeyDSIGN BLS12381MinSigDSIGN
forall a. HasCallStack => [Char] -> a
error [Char]
"Failed to convert an Agda VerKey to a Haskell VerKey")
            (Maybe (VerKeyDSIGN BLS12381MinSigDSIGN)
 -> VerKeyDSIGN BLS12381MinSigDSIGN)
-> (Integer -> Maybe (VerKeyDSIGN BLS12381MinSigDSIGN))
-> Integer
-> VerKeyDSIGN BLS12381MinSigDSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Maybe (VerKeyDSIGN BLS12381MinSigDSIGN)
forall v. DSIGNAlgorithm v => Integer -> Maybe (VerKeyDSIGN v)
verkeyFromInteger96
            (Integer -> VerKeyDSIGN BLS12381MinSigDSIGN)
-> Integer -> VerKeyDSIGN BLS12381MinSigDSIGN
forall a b. (a -> b) -> a -> b
$ Integer
vk

        proofofpossesion :: PossessionProofDSIGN BLS12381MinSigDSIGN
        proofofpossesion :: PossessionProofDSIGN BLS12381MinSigDSIGN
proofofpossesion =
          PossessionProofDSIGN BLS12381MinSigDSIGN
-> Maybe (PossessionProofDSIGN BLS12381MinSigDSIGN)
-> PossessionProofDSIGN BLS12381MinSigDSIGN
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> PossessionProofDSIGN BLS12381MinSigDSIGN
forall a. HasCallStack => [Char] -> a
error [Char]
"Failed to decode the PoP")
            (Maybe (PossessionProofDSIGN BLS12381MinSigDSIGN)
 -> PossessionProofDSIGN BLS12381MinSigDSIGN)
-> (Integer -> Maybe (PossessionProofDSIGN BLS12381MinSigDSIGN))
-> Integer
-> PossessionProofDSIGN BLS12381MinSigDSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Maybe (PossessionProofDSIGN BLS12381MinSigDSIGN)
forall v.
DSIGNAggregatable v =>
Integer -> Maybe (PossessionProofDSIGN v)
popFromInteger
            (Integer -> PossessionProofDSIGN BLS12381MinSigDSIGN)
-> Integer -> PossessionProofDSIGN BLS12381MinSigDSIGN
forall a b. (a -> b) -> a -> b
$ Integer
pop

    extValidPlutusScript :: Bool
extValidPlutusScript = Bool
True