{-# OPTIONS --safe #-}
module Ledger.Dijkstra.Specification.Transaction where

import Data.Maybe.Base as M

open import Ledger.Prelude renaming (filterᵐ to filter)

open import Ledger.Core.Specification.Crypto
open import Ledger.Core.Specification.Epoch
open import Ledger.Dijkstra.Specification.Gov.Base

import Ledger.Core.Specification.Address renaming (RewardAddress to RewardAddress)
import Ledger.Dijkstra.Specification.Certs
import Ledger.Dijkstra.Specification.Gov.Actions
import Ledger.Dijkstra.Specification.PParams
import Ledger.Dijkstra.Specification.Script
import Ledger.Dijkstra.Specification.TokenAlgebra.Base

open import Tactic.Derive.DecEq
open import Relation.Nullary.Decidable using (⌊_⌋)


data TxLevel : Type where
  TxLevelTop TxLevelSub : TxLevel


InTopLevel : TxLevel → Type → Type
InTopLevel TxLevelTop X = X
InTopLevel TxLevelSub _ = ⊤

InSubLevel : TxLevel → Type → Type
InSubLevel TxLevelSub X = X
InSubLevel TxLevelTop _ = ⊤


unquoteDecl DecEq-TxLevel = derive-DecEq ((quote TxLevel , DecEq-TxLevel) ∷ [])

private
  variable
    txLevel : TxLevel

data Tag : TxLevel → Type where
  Spend Mint Cert Reward Vote Propose Guard : Tag txLevel
  SubGuard : Tag TxLevelSub

unquoteDecl DecEq-Tag = derive-DecEq ((quote Tag , DecEq-Tag) ∷ [])


record TransactionStructure : Type₁ where
  field
    Ix TxId AuxiliaryData  : Type
    adHashingScheme        : isHashableSet AuxiliaryData
    globalConstants        : GlobalConstants
    crypto                 : CryptoStructure
    epochStructure         : EpochStructure


    ⦃ DecEq-Ix   ⦄ : DecEq Ix
    ⦃ DecEq-TxId ⦄ : DecEq TxId
  open isHashableSet adHashingScheme renaming (THash to ADHash) public
  open GlobalConstants globalConstants public
  open CryptoStructure crypto public
  open Ledger.Dijkstra.Specification.TokenAlgebra.Base ScriptHash public
  open Ledger.Core.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
  open EpochStructure epochStructure public
  open Ledger.Dijkstra.Specification.Script crypto epochStructure public
  field


    scriptStructure        : ScriptStructure


  open ScriptStructure scriptStructure public
  open Ledger.Dijkstra.Specification.PParams crypto epochStructure scriptStructure public
  field


    govParams              : GovParams
    tokenAlgebra           : TokenAlgebra
    txidBytes              : TxId → Ser


  open GovParams govParams public
  open TokenAlgebra tokenAlgebra public


  govStructure : GovStructure
  govStructure = record
    -- TODO: figure out what to do with the hash
    { TxId = TxId; DocHash = ADHash
    ; cryptoStructure = crypto
    ; epochStructure = epochStructure
    ; scriptStructure = scriptStructure
    ; govParams = govParams
    ; globalConstants = globalConstants
    }


  module GovernanceActions = Ledger.Dijkstra.Specification.Gov.Actions govStructure
  open GovernanceActions hiding (Vote; yes; no; abstain) public

  open import Ledger.Dijkstra.Specification.Certs govStructure


  TxIn : Type
  TxIn = TxId × Ix

  TxOut : Type
  TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script

  UTxO : Type
  UTxO = TxIn ⇀ TxOut

  RedeemerPtr : TxLevel → Type
  RedeemerPtr txLevel  = Tag txLevel × Ix

  ProposedPPUpdates : Type
  ProposedPPUpdates = KeyHash ⇀ PParamsUpdate

  Update : Type
  Update = ProposedPPUpdates × Epoch

  record HasUTxO {a} (A : Type a) : Type a where
    field UTxOOf : A → UTxO
  open HasUTxO ⦃...⦄ public


  mutual
    record Tx (txLevel : TxLevel) : Type where
      inductive
      field
        txBody       : TxBody txLevel
        txWitnesses  : TxWitnesses txLevel
        isValid      : InTopLevel txLevel Bool
        txAuxData    : Maybe AuxiliaryData

    record TxBody (txLevel : TxLevel) : Type where
      inductive
      field
        txIns                : ℙ TxIn
        refInputs            : ℙ TxIn
        collateralInputs     : InTopLevel txLevel (ℙ TxIn)
        txOuts               : Ix ⇀ TxOut
        txId                 : TxId
        txCerts              : List DCert
        txFee                : InTopLevel txLevel Fees
        txWithdrawals        : Withdrawals
        txVldt               : Maybe Slot × Maybe Slot
        txADhash             : Maybe ADHash
        txDonation           : Donations
        txGovVotes           : List GovVote
        txGovProposals       : List GovProposal
        txNetworkId          : Maybe Network
        currentTreasury      : Maybe Coin
        mint                 : Value
        scriptIntegrityHash  : Maybe ScriptHash

        -- New in Dijkstra --
        txSubTransactions         : InTopLevel txLevel (List (Tx TxLevelSub))
        txGuards                  : ℙ Credential
        txRequiredTopLevelGuards  : InSubLevel txLevel (ℙ (Credential × Maybe Datum))
        ---------------------

      reqSignerHashes : ℙ KeyHash
      reqSignerHashes = mapPartial isKeyHashObj txGuards


    record TxWitnesses (txLevel : TxLevel) : Type where
      inductive
      field
        vKeySigs     : VKey ⇀ Sig
        scripts      : ℙ Script
        txData       : ℙ Datum
        txRedeemers  : RedeemerPtr txLevel ⇀ Redeemer × ExUnits

      scriptsP1 : ℙ P1Script
      scriptsP1 = mapPartial isInj₁ scripts


  TopLevelTx : Type
  TopLevelTx = Tx TxLevelTop

  SubLevelTx : Type
  SubLevelTx = Tx TxLevelSub


  AnyLevelTx : Type
  AnyLevelTx = TopLevelTx ⊎ SubLevelTx


  -- Level-Dependent Type Classes --
  record HasTxBody {txLevel} {a} (A : Type a) : Type a where
    field TxBodyOf : A → TxBody txLevel
  open HasTxBody  ⦃...⦄ public

  record HasTxWitnesses {txLevel} {a} (A : Type a) : Type a where
    field TxWitnessesOf : A → TxWitnesses txLevel
  open HasTxWitnesses ⦃...⦄ public

  record HasRedeemers {txLevel} {a} (A : Type a) : Type a where
    field RedeemersOf : A → RedeemerPtr txLevel ⇀ Redeemer × ExUnits
  open HasRedeemers ⦃...⦄ public

  -- (top-level only) --
  record HasCollateralInputs {txLevel} {a} (A : Type a) : Type a where
    field CollateralInputsOf : A → InTopLevel txLevel (ℙ TxIn)
  open HasCollateralInputs ⦃...⦄ public

  record HasTxFees {txLevel} {a} (A : Type a) : Type a where
    field TxFeesOf : A → InTopLevel txLevel Fees
  open HasTxFees ⦃...⦄ public

  record HasSubTransactions {txLevel} {a} (A : Type a) : Type a where
    field SubTransactionsOf : A → InTopLevel txLevel (List (Tx TxLevelSub))
  open HasSubTransactions ⦃...⦄ public

  -- (sub-level only) --
  record HasTopLevelGuards {txLevel} {a} (A : Type a) : Type a where
    field TopLevelGuardsOf : A → InSubLevel txLevel (ℙ (Credential × Maybe Datum))
  open HasTopLevelGuards ⦃...⦄ public


  -- Level-Independent Type Classes --
  record HasTxId {a} (A : Type a) : Type a where
    field TxIdOf : A → TxId
  open HasTxId ⦃...⦄ public

  record HasSize {a} (A : Type a) : Type a where
    field SizeOf : A → ℕ
  open HasSize ⦃...⦄ public

  record HasSpendInputs {a} (A : Type a) : Type a where
    field SpendInputsOf : A → ℙ TxIn
  open HasSpendInputs ⦃...⦄ public

  record HasReferenceInputs {a} (A : Type a) : Type a where
    field ReferenceInputsOf : A → ℙ TxIn
  open HasReferenceInputs ⦃...⦄ public

  record HasIndexedOutputs {a} (A : Type a) : Type a where
    field IndexedOutputsOf : A → Ix ⇀ TxOut
  open HasIndexedOutputs ⦃...⦄ public

  record HasMintedValue {a} (A : Type a) : Type a where
    field MintedValueOf : A → Value
  open HasMintedValue ⦃...⦄ public

  record HasFees? {a} (A : Type a) : Type a where
    field FeesOf? : A → Maybe Fees
  open HasFees? ⦃...⦄ public

  record HasDCerts {a} (A : Type a) : Type a where
    field DCertsOf : A → List DCert
  open HasDCerts ⦃...⦄ public

  record HasData {a} (A : Type a) : Type a where
    field DataOf : A → ℙ Datum
  open HasData ⦃...⦄ public

  record HasGovProposals {a} (A : Type a) : Type a where
    field GovProposalsOf : A → List GovProposal
  open HasGovProposals ⦃...⦄ public

  record HasGovVotes {a} (A : Type a) : Type a where
    field GovVotesOf : A → List GovVote
  open HasGovVotes ⦃...⦄ public

  record HasGuards {a} (A : Type a) : Type a where
    field GuardsOf : A → ℙ Credential
  open HasGuards ⦃...⦄ public

  record HasScripts {a} (A : Type a) : Type a where
    field ScriptsOf : A → ℙ Script
  open HasScripts ⦃...⦄ public

  record HasTxOuts {a} (A : Type a) : Type a where
    field TxOutsOf : A → Ix ⇀ TxOut
  open HasTxOuts ⦃...⦄ public

  instance
    HasTxBody-Tx : HasTxBody (Tx txLevel)
    HasTxBody-Tx .TxBodyOf = Tx.txBody

    HasTxWitnesses-Tx : HasTxWitnesses (Tx txLevel)
    HasTxWitnesses-Tx .TxWitnessesOf = Tx.txWitnesses

    HasRedeemers-TxWitnesses : HasRedeemers (TxWitnesses txLevel)
    HasRedeemers-TxWitnesses .RedeemersOf = TxWitnesses.txRedeemers

    HasRedeemers-Tx : HasRedeemers (Tx txLevel)
    HasRedeemers-Tx .RedeemersOf = RedeemersOf ∘ TxWitnessesOf

    HasCollateralInputs-TopLevelTx : HasCollateralInputs TopLevelTx
    HasCollateralInputs-TopLevelTx .CollateralInputsOf = TxBody.collateralInputs ∘ TxBodyOf

    HasTxFees-TopLevelTx : HasTxFees TopLevelTx
    HasTxFees-TopLevelTx .TxFeesOf = TxBody.txFee ∘ TxBodyOf

    HasSubTransactions-TopLevelTx : HasSubTransactions TopLevelTx
    HasSubTransactions-TopLevelTx .SubTransactionsOf = TxBody.txSubTransactions ∘ TxBodyOf

    HasTopLevelGuards-SubLevelTx : HasTopLevelGuards SubLevelTx
    HasTopLevelGuards-SubLevelTx .TopLevelGuardsOf = TxBody.txRequiredTopLevelGuards ∘ TxBodyOf

    HasDCerts-TxBody : HasDCerts (TxBody txLevel)
    HasDCerts-TxBody .DCertsOf = TxBody.txCerts

    HasDCerts-Tx : HasDCerts (Tx txLevel)
    HasDCerts-Tx .DCertsOf = DCertsOf ∘ TxBodyOf

    HasWithdrawals-TxBody : HasWithdrawals (TxBody txLevel)
    HasWithdrawals-TxBody .WithdrawalsOf = TxBody.txWithdrawals

    HasWithdrawals-Tx : HasWithdrawals (Tx txLevel)
    HasWithdrawals-Tx .WithdrawalsOf = WithdrawalsOf ∘ TxBodyOf

    HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
    HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns

    HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
    HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf

    HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
    HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.refInputs

    HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
    HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf

    HasIndexedOutputs-TxBody : HasIndexedOutputs (TxBody txLevel)
    HasIndexedOutputs-TxBody .IndexedOutputsOf = TxBody.txOuts

    HasIndexedOutputs-Tx : HasIndexedOutputs (Tx txLevel)
    HasIndexedOutputs-Tx .IndexedOutputsOf = IndexedOutputsOf ∘ TxBodyOf

    HasMintedValue-TxBody : HasMintedValue (TxBody txLevel)
    HasMintedValue-TxBody .MintedValueOf = TxBody.mint

    HasMintedValue-Tx : HasMintedValue (Tx txLevel)
    HasMintedValue-Tx .MintedValueOf = MintedValueOf ∘ TxBodyOf

    HasGovVotes-TxBody : HasGovVotes (TxBody txLevel)
    HasGovVotes-TxBody .GovVotesOf = TxBody.txGovVotes

    HasGovVotes-Tx : HasGovVotes (Tx txLevel)
    HasGovVotes-Tx .GovVotesOf = GovVotesOf ∘ TxBodyOf

    HasGovProposals-TxBody : HasGovProposals (TxBody txLevel)
    HasGovProposals-TxBody .GovProposalsOf = TxBody.txGovProposals

    HasGovProposals-Tx : HasGovProposals (Tx txLevel)
    HasGovProposals-Tx .GovProposalsOf = GovProposalsOf ∘ TxBodyOf

    HasFees?-TxBody : {ℓ : TxLevel} → HasFees? (TxBody ℓ)
    HasFees?-TxBody {TxLevelTop} .FeesOf? tbTop = just (TxBody.txFee tbTop)
    HasFees?-TxBody {TxLevelSub} .FeesOf? tbSub = nothing

    HasFees?-Tx : HasFees? (Tx txLevel)
    HasFees?-Tx .FeesOf? = FeesOf? ∘ TxBodyOf

    HasTxId-TxBody : HasTxId (TxBody txLevel)
    HasTxId-TxBody .TxIdOf = TxBody.txId

    HasTxId-Tx : HasTxId (Tx txLevel)
    HasTxId-Tx .TxIdOf = TxIdOf ∘ TxBodyOf

    HasDonations-TxBody : HasDonations (TxBody txLevel)
    HasDonations-TxBody .DonationsOf = TxBody.txDonation

    HasDonations-Tx : HasDonations (Tx txLevel)
    HasDonations-Tx .DonationsOf = DonationsOf ∘ TxBodyOf

    HasCoin-TxOut : HasCoin TxOut
    HasCoin-TxOut .getCoin = coin ∘ proj₁ ∘ proj₂

    HasData-TxWitnesses : HasData (TxWitnesses txLevel)
    HasData-TxWitnesses .DataOf = TxWitnesses.txData

    HasData-Tx : HasData (Tx txLevel)
    HasData-Tx .DataOf = DataOf ∘ TxWitnessesOf

    HasGuards-TxBody : HasGuards (TxBody txLevel)
    HasGuards-TxBody .GuardsOf = TxBody.txGuards

    HasGuards-Tx : HasGuards (Tx txLevel)
    HasGuards-Tx .GuardsOf = GuardsOf ∘ TxBodyOf

    HasScripts-TxWitnesses : HasScripts (TxWitnesses txLevel)
    HasScripts-TxWitnesses .ScriptsOf = TxWitnesses.scripts

    HasScripts-Tx : HasScripts (Tx txLevel)
    HasScripts-Tx .ScriptsOf = ScriptsOf ∘ TxWitnessesOf

    HasTxOuts-TxBody : HasTxOuts (TxBody txLevel)
    HasTxOuts-TxBody .TxOutsOf = TxBody.txOuts

    HasTxOuts-Tx : HasTxOuts (Tx txLevel)
    HasTxOuts-Tx .TxOutsOf = TxOutsOf ∘ TxBodyOf


  getValue : TxOut → Value
  getValue (_ , v , _) = v

  TxOutʰ : Type
  TxOutʰ = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe ScriptHash

  txOutHash : TxOut → TxOutʰ
  txOutHash (a , v , d , s) = a , (v , (d , M.map hash s))

  getValueʰ : TxOutʰ → Value
  getValueʰ (_ , v , _) = v

  txinsVKey : ℙ TxIn → UTxO → ℙ TxIn
  txinsVKey txins utxo = txins ∩ dom (utxo ∣^' (isVKeyAddr ∘ proj₁))

  scriptOuts : UTxO → UTxO
  scriptOuts utxo = filter (λ (_ , addr , _) → isScriptAddr addr) utxo

  txinsScript : ℙ TxIn → UTxO → ℙ TxIn
  txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))


  txOutToScript : TxOut → Maybe Script
  txOutToScript (_ , _ , _ , s) = s

  getTxScripts : UTxO → Tx txLevel → ℙ Script
  getTxScripts utxo tx =
    ScriptsOf tx                              -- (1) scripts from witnesses
    ∪ mapPartial txOutToScript
       ( range (utxo ∣ SpendInputsOf tx)      -- (2) scripts from spending inputs
       ∪ range (utxo ∣ ReferenceInputsOf tx)  -- (3) scripts from reference inputs
       ∪ range (TxOutsOf tx ˢ))                -- (4) scripts from transaction outputs

  getAllScripts : TopLevelTx → UTxO → ℙ P1Script × ℙ P2Script
  getAllScripts tx utxo = mapPartial toP1Script allScripts , mapPartial toP2Script allScripts
    where
      allScripts : ℙ Script
      allScripts = getTxScripts utxo tx                                               -- (1) scripts from top-level transaction
                   ∪ concatMapˢ (getTxScripts utxo) (fromList (SubTransactionsOf tx))  -- (2) scripts from subtransactions

  lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script
  lookupScriptHash sh tx utxoSpend₀ utxoRefView = lookupHash sh (getTxScripts utxoRefView tx)

  txOutToDatum : TxOut → Maybe Datum
  txOutToDatum (_ , _ , d , _) = d >>= isInj₁

  getTxData : UTxO → Tx txLevel → ℙ Datum
  getTxData utxo tx =
    DataOf tx                                 -- (1) data from witnesses
    ∪ mapPartial txOutToDatum
       ( range (utxo ∣ SpendInputsOf tx)      -- (2) data from spending inputs
       ∪ range (utxo ∣ ReferenceInputsOf tx)  -- (3) data from reference inputs
       ∪ range (TxOutsOf tx ˢ))                -- (4) data from transaction outputs

  getAllData : TopLevelTx → UTxO → ℙ Datum
  getAllData tx utxo = getTxData utxo tx
                       ∪ concatMapˢ (getTxData utxo) (fromList (SubTransactionsOf tx))


  TaggedTopLevelGuard : Type
  TaggedTopLevelGuard = TxId × Credential × Maybe Datum
                     -- (subTxId, guard credential, optional datum argument)

  GroupedTopLevelGuards : Type
  GroupedTopLevelGuards = List (Credential × List (TxId × Maybe Datum))

  groupTopLevelGuards : List TaggedTopLevelGuard → GroupedTopLevelGuards
  groupTopLevelGuards = foldr insertGuard []
    where
    -- Insert one tagged guard into an existing group:
    --   + if the credential already has a group, cons (subTxId, datum?) onto its list
    --   + otherwise create a new group for that credential.
    insertGuard : TaggedTopLevelGuard → GroupedTopLevelGuards → GroupedTopLevelGuards
    insertGuard (tid , cred , md) [] = (cred , (tid , md) ∷ []) ∷ []
    insertGuard (tid , cred , md) ((c , xs) ∷ rest) with c ≟ cred
    ... | yes _ = (c , (tid , md) ∷ xs) ∷ rest
    ... | no  _ = (c , xs) ∷ insertGuard (tid , cred , md) rest

  subTxTaggedGuards : SubLevelTx → ℙ TaggedTopLevelGuard
  subTxTaggedGuards subtx =
    mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md)) (TopLevelGuardsOf subtx)

  -- Turn a subTx body's `txRequiredTopLevelGuards` into a set of guard credentials.
  subTxGuardCredentials : SubLevelTx → ℙ Credential
  subTxGuardCredentials = (mapˢ proj₁) ∘ TopLevelGuardsOf

  -- Phase-1 condition (CIP-0118):
  -- every credential required by a subTx body must appear in the top-level txGuards set.
  requiredTopLevelGuardsSatisfied : TopLevelTx → List SubLevelTx → Type
  requiredTopLevelGuardsSatisfied topTx subTxs = requiredCreds ⊆ GuardsOf topTx
    where
    concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B
    concatMapˡ f as = proj₁ $ unions (fromList (map f as))
    -- (maybe move concatMapˡ to src-lib-exts or agda-sets)

    requiredCreds : ℙ Credential
    requiredCreds = concatMapˡ subTxGuardCredentials subTxs