{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger () where

import Cardano.Ledger.Alonzo.Tx (AlonzoStAnnTx)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  AllegraEraTxBody (..),
  AlonzoEraTx (..),
  AlonzoEraTxBody (..),
  BabbageEraTxBody (..),
  ConwayEraTxBody (..),
  EraTx (..),
  EraTxBody (..),
  ScriptHash,
  TxLevel (..),
  txIdTx,
  txStAnnTxG,
 )
import qualified Cardano.Ledger.Conway.Rules as Conway
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import Cardano.Ledger.TxIn (TxId)
import Data.Maybe.Strict (StrictMaybe)
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (askSpecTransM, withCtxSpecTransM)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  SpecTranslate (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()

instance SpecTranslate ConwayEra (Shelley.LedgerEnv ConwayEra) where
  type SpecRep ConwayEra (Shelley.LedgerEnv ConwayEra) = Agda.LEnv
  type
    SpecContext ConwayEra (Shelley.LedgerEnv ConwayEra) =
      (StrictMaybe ScriptHash, Conway.EnactState ConwayEra)

  toSpecRep :: LedgerEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (LedgerEnv ConwayEra))
     (SpecRep ConwayEra (LedgerEnv ConwayEra))
toSpecRep Shelley.LedgerEnv {Maybe EpochNo
PParams ConwayEra
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams ConwayEra
ledgerAccount :: ChainAccountState
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
..} = do
    (policyHash, enactState) <- SpecTransM
  ConwayEra
  (StrictMaybe ScriptHash, EnactState ConwayEra)
  (StrictMaybe ScriptHash, EnactState ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkLEnv
        <$> toSpecRep ledgerSlotNo
        <*> toSpecRep policyHash
        <*> toSpecRep ledgerPp
        <*> toSpecRep enactState
        <*> toSpecRep (casTreasury ledgerAccount)

instance SpecTranslate ConwayEra (TxBody TopTx ConwayEra) where
  type SpecRep ConwayEra (TxBody TopTx ConwayEra) = Agda.TxBody
  type SpecContext ConwayEra (TxBody TopTx ConwayEra) = TxId

  toSpecRep :: TxBody TopTx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (TxBody TopTx ConwayEra))
     (SpecRep ConwayEra (TxBody TopTx ConwayEra))
toSpecRep TxBody TopTx ConwayEra
txb = do
    txId <- SpecTransM ConwayEra TxId TxId
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    withCtxSpecTransM () $
      Agda.MkTxBody
        <$> toSpecRep (txb ^. inputsTxBodyL)
        <*> toSpecRep (txb ^. referenceInputsTxBodyL)
        <*> toSpecRep (txb ^. collateralInputsTxBodyL)
        <*> (Agda.MkHSMap . zip [0 ..] <$> toSpecRep (txb ^. outputsTxBodyL))
        <*> toSpecRep txId
        <*> toSpecRep (txb ^. certsTxBodyL)
        <*> toSpecRep (txb ^. feeTxBodyL)
        <*> toSpecRep (txb ^. withdrawalsTxBodyL)
        <*> toSpecRep (txb ^. vldtTxBodyL)
        <*> toSpecRep (txb ^. auxDataHashTxBodyL)
        <*> toSpecRep (txb ^. treasuryDonationTxBodyL)
        <*> toSpecRep (txb ^. votingProceduresTxBodyL)
        <*> toSpecRep (txb ^. proposalProceduresTxBodyL)
        <*> toSpecRep (txb ^. networkIdTxBodyL)
        <*> toSpecRep (txb ^. currentTreasuryValueTxBodyL)
        <*> pure 0
        <*> toSpecRep (txb ^. reqSignerHashesTxBodyL)
        -- The script integrity hash is computed using @const 0@ on the Agda
        -- side (@Hashable-ScriptIntegrity = record { hash = λ x → 0 }@).
        -- Until a proper hash function is used in Agda, we emulate the same
        -- behavior here.
        --
        -- The following PR documents the discrepancy on the Agda side:
        -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/1086
        <*> fmap (fmap (const 0)) (toSpecRep (txb ^. scriptIntegrityHashTxBodyL))

instance SpecTranslate ConwayEra (Tx TopTx ConwayEra) where
  type SpecRep ConwayEra (Tx TopTx ConwayEra) = Agda.Tx

  toSpecRep :: Tx TopTx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Tx TopTx ConwayEra))
     (SpecRep ConwayEra (Tx TopTx ConwayEra))
toSpecRep Tx TopTx ConwayEra
tx =
    TxBody -> TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx
Agda.MkTx
      (TxBody -> TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ConwayEra () TxBody
-> SpecTransM
     ConwayEra
     ()
     (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxId
-> SpecTransM ConwayEra TxId TxBody
-> SpecTransM ConwayEra () TxBody
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM (Tx TopTx ConwayEra -> TxId
forall era (l :: TxLevel). EraTx era => Tx l era -> TxId
txIdTx Tx TopTx ConwayEra
tx) (TxBody TopTx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (TxBody TopTx ConwayEra))
     (SpecRep ConwayEra (TxBody TopTx ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (TxBody TopTx ConwayEra)
     (Tx TopTx ConwayEra)
     (TxBody TopTx ConwayEra)
-> TxBody TopTx ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (TxBody TopTx ConwayEra)
  (Tx TopTx ConwayEra)
  (TxBody TopTx ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l ConwayEra) (TxBody l ConwayEra)
bodyTxL))
      SpecTransM
  ConwayEra
  ()
  (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ConwayEra () TxWitnesses
-> SpecTransM ConwayEra () (Integer -> Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AlonzoTxWits ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (AlonzoTxWits ConwayEra))
     (SpecRep ConwayEra (AlonzoTxWits ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (AlonzoTxWits ConwayEra)
     (Tx TopTx ConwayEra)
     (AlonzoTxWits ConwayEra)
-> AlonzoTxWits ConwayEra
forall s a. s -> Getting a s a -> a
^. (TxWits ConwayEra
 -> Const (AlonzoTxWits ConwayEra) (TxWits ConwayEra))
-> Tx TopTx ConwayEra
-> Const (AlonzoTxWits ConwayEra) (Tx TopTx ConwayEra)
Getting
  (AlonzoTxWits ConwayEra)
  (Tx TopTx ConwayEra)
  (AlonzoTxWits ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l ConwayEra) (TxWits ConwayEra)
witsTxL)
      SpecTransM ConwayEra () (Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word32
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Word32) (SpecRep ConwayEra Word32)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting Word32 (Tx TopTx ConwayEra) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx TopTx ConwayEra) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx TopTx ConwayEra) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l ConwayEra) Word32
sizeTxF)
      SpecTransM ConwayEra () (Bool -> Maybe Integer -> Tx)
-> SpecTransM ConwayEra () Bool
-> SpecTransM ConwayEra () (Maybe Integer -> Tx)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IsValid
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra IsValid)
     (SpecRep ConwayEra IsValid)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting IsValid (Tx TopTx ConwayEra) IsValid -> IsValid
forall s a. s -> Getting a s a -> a
^. Getting IsValid (Tx TopTx ConwayEra) IsValid
forall era. AlonzoEraTx era => Lens' (Tx TopTx era) IsValid
Lens' (Tx TopTx ConwayEra) IsValid
isValidTxL)
      SpecTransM ConwayEra () (Maybe Integer -> Tx)
-> SpecTransM ConwayEra () (Maybe Integer)
-> SpecTransM ConwayEra () Tx
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (AlonzoTxAuxData ConwayEra)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (StrictMaybe (AlonzoTxAuxData ConwayEra)))
     (SpecRep ConwayEra (StrictMaybe (AlonzoTxAuxData ConwayEra)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Tx TopTx ConwayEra
tx Tx TopTx ConwayEra
-> Getting
     (StrictMaybe (AlonzoTxAuxData ConwayEra))
     (Tx TopTx ConwayEra)
     (StrictMaybe (AlonzoTxAuxData ConwayEra))
-> StrictMaybe (AlonzoTxAuxData ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictMaybe (TxAuxData ConwayEra)
 -> Const
      (StrictMaybe (AlonzoTxAuxData ConwayEra))
      (StrictMaybe (TxAuxData ConwayEra)))
-> Tx TopTx ConwayEra
-> Const
     (StrictMaybe (AlonzoTxAuxData ConwayEra)) (Tx TopTx ConwayEra)
Getting
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
  (Tx TopTx ConwayEra)
  (StrictMaybe (AlonzoTxAuxData ConwayEra))
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (StrictMaybe (TxAuxData era))
forall (l :: TxLevel).
Lens' (Tx l ConwayEra) (StrictMaybe (TxAuxData ConwayEra))
auxDataTxL)

instance SpecTranslate ConwayEra (AlonzoStAnnTx TopTx ConwayEra) where
  type SpecRep ConwayEra (AlonzoStAnnTx TopTx ConwayEra) = Agda.Tx

  toSpecRep :: AlonzoStAnnTx TopTx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (AlonzoStAnnTx TopTx ConwayEra))
     (SpecRep ConwayEra (AlonzoStAnnTx TopTx ConwayEra))
toSpecRep AlonzoStAnnTx TopTx ConwayEra
stAnnTx = Tx TopTx ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Tx TopTx ConwayEra))
     (SpecRep ConwayEra (Tx TopTx ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (AlonzoStAnnTx TopTx ConwayEra
stAnnTx AlonzoStAnnTx TopTx ConwayEra
-> Getting
     (Tx TopTx ConwayEra)
     (AlonzoStAnnTx TopTx ConwayEra)
     (Tx TopTx ConwayEra)
-> Tx TopTx ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (Tx TopTx ConwayEra) (StAnnTx TopTx ConwayEra) (Tx TopTx ConwayEra)
Getting
  (Tx TopTx ConwayEra)
  (AlonzoStAnnTx TopTx ConwayEra)
  (Tx TopTx ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
SimpleGetter (StAnnTx l era) (Tx l era)
forall (l :: TxLevel).
SimpleGetter (StAnnTx l ConwayEra) (Tx l ConwayEra)
txStAnnTxG)