{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction
open import Ledger.Dijkstra.Specification.Abstract

module Ledger.Dijkstra.Specification.Script.Validation
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp)
  where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Certs govStructure

open import Ledger.Dijkstra.Specification.Abstract txs
open import Ledger.Dijkstra.Specification.Script.ScriptPurpose txs

open import Data.List using (fromMaybe)


private variable
  ℓ : TxLevel


rdptr : Tx ℓ → ScriptPurpose → Maybe (RedeemerPtr ℓ)
rdptr tx = λ where
  (Cert h)     → map (Cert     ,_) $ indexOfDCert           h (DCertsOf tx)
  (Rwrd h)     → map (Reward   ,_) $ indexOfRewardAddress   h (WithdrawalsOf tx)
  (Mint h)     → map (Mint     ,_) $ indexOfPolicyId        h (policies (MintedValueOf tx))
  (Spend h)    → map (Spend    ,_) $ indexOfTxIn            h (SpendInputsOf tx)
  (Vote h)     → map (Vote     ,_) $ indexOfVote            h (map GovVote.voter (ListOfGovVotesOf tx))
  (Propose h)  → map (Propose  ,_) $ indexOfProposal        h (ListOfGovProposalsOf tx)
  (Guard c)    → map (Guard    ,_) $ indexOfGuard           c (map proj₁ (setToList (GuardsOf tx)))

indexedRdmrs : Tx ℓ → ScriptPurpose → Maybe (Redeemer × ExUnits)
indexedRdmrs tx sp = maybe (λ x → lookupᵐ? (RedeemersOf tx) x) nothing (rdptr tx sp)


getDatumSpend
  : Tx ℓ
  → UTxO
  → (DataHash ⇀ Datum)
  → TxIn
  → Maybe Datum
getDatumSpend tx utxo₀ allData txin
  with lookupᵐ? utxo₀ txin
... | just (_ , _ , just d , _) =
  case d of λ where
    (inj₁ d) → just d
    (inj₂ h) → lookupᵐ? allData h
... | _ = nothing


getDataGuard
  : Tx ℓ
  → UTxO
  → Credential
  → ℙ Datum × Bool
getDataGuard tx utxo₀ c
  = mapPartial (λ (c' , d) → if c ≡ c' then d else nothing) (GuardsOf tx)
    , ¿ (c , nothing) ∈ GuardsOf tx ¿ᵇ


txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo

txInfo TxLevelTop utxo tx =
  record  { realizedInputs  = utxo ∣ (SpendInputsOf tx)
          ; txOuts          = TxOutsOf tx
          ; txFee           = FeesOf? tx
          ; mint            = MintedValueOf tx
          ; txCerts         = DCertsOf tx
          ; txWithdrawals   = WithdrawalsOf tx
          ; txVldt          = ValidIntervalOf tx
          ; vkKey           = RequiredSignerHashesOf tx
          ; txGuards        = GuardsOf tx
          ; txData          = DataOf tx
          ; txId            = TxIdOf tx
          ; txInfoSubTxs    = nothing
          }

txInfo TxLevelSub utxo tx =
  record  { realizedInputs  = utxo ∣ (TxBody.txIns txBody)
          ; txOuts          = TxBody.txOuts txBody
          ; txFee           = nothing
          ; mint            = TxBody.mint txBody
          ; txCerts         = TxBody.txCerts txBody
          ; txWithdrawals   = TxBody.txWithdrawals txBody
          ; txVldt          = TxBody.txVldt txBody
          ; vkKey           = TxBody.requiredSignerHashes txBody
          ; txGuards        = TxBody.txGuards txBody
          ; txData          = DataOf tx
          ; txId            = TxBody.txId txBody
          ; txInfoSubTxs    = nothing
          } where open Tx tx

txInfoForPurpose : {ℓ : TxLevel} → UTxO → Tx ℓ → ScriptPurpose → TxInfo

-- subtransactions: never get subTx infos (even if the ScriptPurpose is Guard).
txInfoForPurpose {TxLevelSub} utxo tx _ = txInfo TxLevelSub utxo tx

-- top-level transactions:
txInfoForPurpose {TxLevelTop} utxo tx sp with sp
   -- · guard scripts see subTx infos
... | Guard _ =  record base { txInfoSubTxs = just subInfos }
                 where
                 base : TxInfo
                 base = txInfo TxLevelTop utxo tx
                 subInfos : List SubTxInfo
                 subInfos = map (txInfo TxLevelSub utxo) (SubTransactionsOf tx)
   -- · other top-level scripts see no subTx infos
... | _ = txInfo TxLevelTop utxo tx

txOutToDataHash : TxOut → Maybe DataHash
txOutToDataHash (_ , _ , d , _) = d >>= isInj₂


credsNeeded : UTxO → Tx ℓ → ℙ (ScriptPurpose × Credential)
credsNeeded utxo tx =
    mapˢ        (λ (i , o) → (Spend  i , payCred (proj₁ o)))  ((utxo ∣ (SpendInputsOf tx ∪ collateralInputs tx)) ˢ)
  ∪ mapˢ        (λ a →      (Rwrd a , CredentialOf a))        (dom ∣ WithdrawalsOf tx ∣)
  ∪ mapPartial  (λ c →      (Cert c ,_) <$> cwitness c)       (fromList (DCertsOf tx))
  ∪ mapˢ        (λ x →      (Mint x , ScriptObj x))           (policies (MintedValueOf tx))
  ∪ mapˢ        (λ v →      (Vote v , govVoterCredential v))  (fromList (map GovVoterOf (ListOfGovVotesOf tx)))
  ∪ mapPartial  (λ p →  if PolicyOf p then (λ {sh} → just (Propose  p , ScriptObj sh))
                        else nothing)                         (fromList (ListOfGovProposalsOf tx))
  ∪ mapˢ        (λ (c , d) → (Guard c , c))                  (GuardsOf tx)
  where
    collateralInputs : Tx ℓ → ℙ TxIn
    collateralInputs {TxLevelTop} tx = CollateralInputsOf tx
    collateralInputs {TxLevelSub} tx = ∅


opaque


  collectP2ScriptsWithContext
    : PParams
    → Tx ℓ
    → UTxO
    → (DataHash ⇀ Datum)
    → ℙ Script
    → List (P2Script × List Data × ExUnits × CostModel)
  collectP2ScriptsWithContext pp tx utxo allData allScripts
    = concat (setToList (mapˢ toScript (credsNeeded utxo tx)))
    where
      context : ScriptPurpose → Data
      context sp = valContext (txInfoForPurpose utxo tx sp) sp

      getScript : Credential → ScriptPurpose → Maybe (P2Script × Redeemer × ExUnits × CostModel)
      getScript c sp = do
             script               ← isScriptObj c >>= λ sh → lookupHash sh allScripts >>= toP2Script
             (reedemer , exUnits) ← indexedRdmrs tx sp
             costModel            ← lookupᵐ? (PParams.costmdls pp) (language script)
             return (script , reedemer , exUnits , costModel)

      assembleData : Redeemer → ScriptPurpose → List (List Data)
      assembleData redeemer sp@(Spend txin)
        = [ fromMaybe (getDatumSpend tx utxo allData txin) ++ (redeemer ∷ [ context sp ]) ]
      assembleData redeemer sp@(Guard c) =
        let data′ , withoutDatum = getDataGuard tx utxo c
        in  map (λ d → [ d ] ++ (redeemer ∷ [ context sp ])) (setToList data′)
            ++ (if withoutDatum then [(redeemer ∷ [ context sp ])]
                                else [])
      assembleData redeemer sp           = [ redeemer ∷ [ context sp ] ]

      toScript
        : ScriptPurpose × Credential
        → List (P2Script × List Data × ExUnits × CostModel)
      toScript (sp , c) =
        do (script , reedemer , exUnits , costModel) ← fromMaybe (getScript c sp)
           data′ ← assembleData reedemer sp
           [ (script , data′ , exUnits , costModel) ]

evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool
evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d)