Utxo

{-# OPTIONS --no-qualified-instances #-}

module Ledger.Conway.Foreign.Utxo where

open import Foreign.Convertible 
open import Foreign.Convertible.Deriving
open import Foreign.Haskell
open import Foreign.Haskell.Coerce
open import Foreign.HaskellTypes
open import Foreign.HaskellTypes.Deriving

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes

open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length; map; fromList)

open import Ledger.Core.Foreign.Address
open import Ledger.Core.Foreign.Crypto
open import Ledger.Conway.Foreign.HSStructures hiding (TxWitnesses; isScriptObj; isKeyHashObj; refScripts)
open import Ledger.Conway.Foreign.Certs
open import Ledger.Conway.Foreign.PParams
open import Ledger.Conway.Foreign.Transaction
open import Ledger.Core.Foreign.ExternalFunctions

open import Ledger.Conway.Foreign.HSStructures hiding (TxWitnesses; refScripts; isScriptObj; isKeyHashObj)
open import Ledger.Conway.Specification.Script.Validation DummyTransactionStructure DummyAbstractFunctions
open import Ledger.Conway.Conformance.Utxo DummyTransactionStructure DummyAbstractFunctions
open import Ledger.Conway.Conformance.Utxow DummyTransactionStructure DummyAbstractFunctions

open Computational

instance
  HsTy-UTxOEnv = autoHsType UTxOEnv ⊣ withConstructor "MkUTxOEnv"
                                    • fieldPrefix "ue"
  Conv-UTxOEnv = autoConvert UTxOEnv

  HsTy-UTxOState = autoHsType UTxOState ⊣ withConstructor "MkUTxOState"
  Conv-UTxOState = autoConvert UTxOState

unquoteDecl = do
  hsTypeAlias UTxO
  hsTypeAlias Redeemer

module _ (ext : ExternalFunctions) where
  open import Ledger.Conway.Foreign.ExternalStructures ext hiding (Tx; TxBody; inject)
  open import Ledger.Conway.Conformance.Utxow.Properties HSTransactionStructure HSAbstractFunctions
  open import Ledger.Conway.Conformance.Utxo.Properties HSTransactionStructure HSAbstractFunctions

  utxo-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState)
  utxo-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXO)

  {-# COMPILE GHC utxo-step as utxoStep #-}

  utxow-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState)
  utxow-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXOW)

  {-# COMPILE GHC utxow-step as utxowStep #-}

  utxo-debug : HsType (UTxOEnv → UTxOState → Tx → String)
  utxo-debug env st tx =
    let open Tx (from tx)
        open TxBody body
        open UTxOState (from st)
        open UTxOEnv (from env)
     in unlines $
          "Consumed:" ∷
          ("\tInputs:      \t" +ˢ show (balance (utxo ∣ txIns))) ∷
          ("\tMint:        \t" +ˢ show mint) ∷
          ("\tRefunds:     \t" +ˢ show (inject (depositRefunds pparams (from st) body))) ∷
          ("\tWithdrawals: \t" +ˢ show (inject (getCoin txWithdrawals))) ∷
          ("\tTotal:       \t" +ˢ show (consumed pparams (from st) body)) ∷
          "Produced:" ∷
          ("\tOutputs:     \t" +ˢ show (balance (outs body))) ∷
          ("\tDonations:   \t" +ˢ show (inject txDonation)) ∷
          ("\tDeposits:    \t" +ˢ show (inject (newDeposits pparams (from st) body))) ∷
          ("\tFees:        \t" +ˢ show (inject txFee)) ∷
          ("\tTotal:       \t" +ˢ show (produced pparams (from st) body)) ∷
          "" ∷
          "Reference Scripts Info:" ∷
          ("\tTotal size: \t" +ˢ show (refScriptsSize utxo (from tx))) ∷
          []

  {-# COMPILE GHC utxo-debug as utxoDebug #-}

  utxow-debug : HsType (UTxOEnv → UTxOState → Tx → String)
  utxow-debug env st tx =
    let open Tx (from tx)
        open TxBody body
        open UTxOState (from st)
        open UTxOEnv (from env)
        open TxWitnesses (coerce ⦃ TrustMe ⦄ wits)
        neededScriptHashes = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo body)
        neededVKeyHashes   = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo body)
        refScriptHashes = mapˢ
          hash 
          (refScripts (coerce ⦃ TrustMe ⦄ (from tx)) (coerce ⦃ TrustMe ⦄ utxo))
        witsScriptHashes  = mapˢ hash scripts
     in unlines
       $ "neededVKeyHashes utxo txb = "
       ∷ show neededVKeyHashes
       ∷ "\nwitsKeyHashes = "
       ∷ show (mapˢ hash (dom vkSigs))
       ∷ "\nneededScriptHashes = "
       ∷ show neededScriptHashes
       ∷ "\nrefScriptHashes = "
       ∷ show refScriptHashes
       ∷ "\nwitsScriptHashes = "
       ∷ show witsScriptHashes
       ∷ []

  {-# COMPILE GHC utxow-debug as utxowDebug #-}