{-# 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 (..),
  EraPParams (..),
  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.Functor.Identity (Identity)
import Data.Maybe.Strict (StrictMaybe)
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.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
  ( EraPParams era
  , SpecTranslate (PParamsHKD Identity era)
  , SpecContext (PParamsHKD Identity era) ~ ()
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  ) =>
  SpecTranslate (Shelley.LedgerEnv era)
  where
  type SpecRep (Shelley.LedgerEnv era) = Agda.LEnv
  type SpecContext (Shelley.LedgerEnv era) = (StrictMaybe ScriptHash, Conway.EnactState era)

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

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

  toSpecRep :: TxBody TopTx ConwayEra
-> SpecTransM
     (SpecContext (TxBody TopTx ConwayEra))
     (SpecRep (TxBody TopTx ConwayEra))
toSpecRep TxBody TopTx ConwayEra
txb = do
    txId <- SpecTransM TxId TxId
forall ctx. SpecTransM 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 (Tx TopTx ConwayEra) where
  type SpecRep (Tx TopTx ConwayEra) = Agda.Tx

  toSpecRep :: Tx TopTx ConwayEra
-> SpecTransM
     (SpecContext (Tx TopTx ConwayEra)) (SpecRep (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 () TxBody
-> SpecTransM
     () (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxId -> SpecTransM TxId TxBody -> SpecTransM () TxBody
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM 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
     (SpecContext (TxBody TopTx ConwayEra))
     (SpecRep (TxBody TopTx ConwayEra))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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
  () (TxWitnesses -> Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM () TxWitnesses
-> SpecTransM () (Integer -> Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AlonzoTxWits ConwayEra
-> SpecTransM
     (SpecContext (AlonzoTxWits ConwayEra))
     (SpecRep (AlonzoTxWits ConwayEra))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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 () (Integer -> Bool -> Maybe Integer -> Tx)
-> SpecTransM () Integer
-> SpecTransM () (Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word32 -> SpecTransM (SpecContext Word32) (SpecRep Word32)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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 () (Bool -> Maybe Integer -> Tx)
-> SpecTransM () Bool -> SpecTransM () (Maybe Integer -> Tx)
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IsValid -> SpecTransM (SpecContext IsValid) (SpecRep IsValid)
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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 () (Maybe Integer -> Tx)
-> SpecTransM () (Maybe Integer) -> SpecTransM () Tx
forall a b.
SpecTransM () (a -> b) -> SpecTransM () a -> SpecTransM () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (AlonzoTxAuxData ConwayEra)
-> SpecTransM
     (SpecContext (StrictMaybe (AlonzoTxAuxData ConwayEra)))
     (SpecRep (StrictMaybe (AlonzoTxAuxData ConwayEra)))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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 (AlonzoStAnnTx TopTx ConwayEra) where
  type SpecRep (AlonzoStAnnTx TopTx ConwayEra) = Agda.Tx

  toSpecRep :: AlonzoStAnnTx TopTx ConwayEra
-> SpecTransM
     (SpecContext (AlonzoStAnnTx TopTx ConwayEra))
     (SpecRep (AlonzoStAnnTx TopTx ConwayEra))
toSpecRep AlonzoStAnnTx TopTx ConwayEra
stAnnTx = Tx TopTx ConwayEra
-> SpecTransM
     (SpecContext (Tx TopTx ConwayEra)) (SpecRep (Tx TopTx ConwayEra))
forall a.
SpecTranslate a =>
a -> SpecTransM (SpecContext a) (SpecRep 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)