{-# OPTIONS --safe #-}

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

module Ledger.Dijkstra.Specification.Utxo
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
open import Ledger.Dijkstra.Specification.Fees using (scriptsCost)

import Data.List.Relation.Unary.All as List
import Data.List.Relation.Unary.AllPairs as List
import Data.Sum.Relation.Unary.All as Sum

private variable
  ℓ : TxLevel

totExUnits : Tx ℓ → ExUnits
totExUnits tx = ∑[ (_ , eu) ← RedeemersOf tx ] eu

-- utxoEntrySizeWithoutVal = 27 words (8 bytes)
utxoEntrySizeWithoutVal : MemoryEstimate
utxoEntrySizeWithoutVal = 8

utxoEntrySize : TxOut → MemoryEstimate
utxoEntrySize (_ , v , _ , _) = utxoEntrySizeWithoutVal + size v

open PParams


record UTxOEnv : Type where
  field
    slot              : Slot
    pparams           : PParams
    treasury          : Treasury
    utxo₀             : UTxO
    depositsChange    : ℤ
    allScripts        : ℙ Script
    allData           : DataHash ⇀ Datum

record SubUTxOEnv : Type where
  field
    slot             : Slot
    pparams          : PParams
    treasury         : Treasury
    utxo₀            : UTxO
    isTopLevelValid  : Bool
    allScripts       : ℙ Script
    allData          : DataHash ⇀ Datum


record UTxOState : Type where
  constructor ⟦_,_,_⟧ᵘ
  field
    utxo       : UTxO
    fees       : Fees
    donations  : Donations


record HasUTxOState {a} (A : Type a) : Type a where
  field UTxOStateOf : A → UTxOState
open HasUTxOState ⦃...⦄ public

record HasIsTopLevelValidFlag {a} (A : Type a) : Type a where
  field IsTopLevelValidFlagOf : A → Bool
open HasIsTopLevelValidFlag ⦃...⦄ public

record HasDepositsChange {a} (A : Type a) : Type a where
  field DepositsChangeOf : A → ℤ
open HasDepositsChange ⦃...⦄ public

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

record HasDataPool {a} (A : Type a) : Type a where
  field DataPoolOf : A → DataHash ⇀ Datum
open HasDataPool ⦃...⦄ public

record HasSlot {a} (A : Type a) : Type a where
  field SlotOf : A → Slot
open HasSlot ⦃...⦄ public

instance
  HasSlot-UTxOEnv : HasSlot UTxOEnv
  HasSlot-UTxOEnv .SlotOf = UTxOEnv.slot

  HasPParams-UTxOEnv : HasPParams UTxOEnv
  HasPParams-UTxOEnv .PParamsOf = UTxOEnv.pparams

  HasTreasury-UTxOEnv : HasTreasury UTxOEnv
  HasTreasury-UTxOEnv .TreasuryOf = UTxOEnv.treasury

  HasUTxO-UTxOEnv : HasUTxO UTxOEnv
  HasUTxO-UTxOEnv .UTxOOf = UTxOEnv.utxo₀

  HasDepositsChange-UTxOEnv : HasDepositsChange UTxOEnv
  HasDepositsChange-UTxOEnv .DepositsChangeOf = UTxOEnv.depositsChange

  HasScriptPool-UTxOEnv : HasScriptPool UTxOEnv
  HasScriptPool-UTxOEnv .ScriptPoolOf = UTxOEnv.allScripts

  HasDataPool-UTxOEnv : HasDataPool UTxOEnv
  HasDataPool-UTxOEnv .DataPoolOf = UTxOEnv.allData

  HasSlot-SubUTxOEnv : HasSlot SubUTxOEnv
  HasSlot-SubUTxOEnv .SlotOf = SubUTxOEnv.slot

  HasPParams-SubUTxOEnv : HasPParams SubUTxOEnv
  HasPParams-SubUTxOEnv .PParamsOf = SubUTxOEnv.pparams

  HasTreasury-SubUTxOEnv : HasTreasury SubUTxOEnv
  HasTreasury-SubUTxOEnv .TreasuryOf = SubUTxOEnv.treasury

  HasUTxO-SubUTxOEnv : HasUTxO SubUTxOEnv
  HasUTxO-SubUTxOEnv .UTxOOf = SubUTxOEnv.utxo₀

  HasIsTopLevelValidFlag-SubUTxOEnv : HasIsTopLevelValidFlag SubUTxOEnv
  HasIsTopLevelValidFlag-SubUTxOEnv .IsTopLevelValidFlagOf = SubUTxOEnv.isTopLevelValid

  HasScriptPool-SubUTxOEnv : HasScriptPool SubUTxOEnv
  HasScriptPool-SubUTxOEnv .ScriptPoolOf = SubUTxOEnv.allScripts

  HasDataPool-SubUTxOEnv : HasDataPool SubUTxOEnv
  HasDataPool-SubUTxOEnv .DataPoolOf = SubUTxOEnv.allData

  HasUTxO-UTxOState : HasUTxO UTxOState
  HasUTxO-UTxOState .UTxOOf = UTxOState.utxo

  HasFee-UTxOState : HasFees UTxOState
  HasFee-UTxOState .FeesOf = UTxOState.fees

  HasDonations-UTxOState : HasDonations UTxOState
  HasDonations-UTxOState .DonationsOf = UTxOState.donations

  unquoteDecl HasCast-UTxOEnv HasCast-SubUTxOEnv HasCast-UTxOState = derive-HasCast
    ( (quote UTxOEnv    , HasCast-UTxOEnv  ) ∷
      (quote SubUTxOEnv , HasCast-SubUTxOEnv  ) ∷
    [ (quote UTxOState  , HasCast-UTxOState) ])


outs : Tx ℓ  → UTxO
outs tx = mapKeys (TxIdOf tx ,_) (TxOutsOf tx)

balance : UTxO → Value
balance utxo = ∑ˢ[ v ← valuesOfUTxO utxo ] v

cbalance : UTxO → Coin
cbalance utxo = coin (balance utxo)

refScriptsSize : TopLevelTx → UTxO → ℕ
refScriptsSize txTop utxo =
 ∑ˡ[ x ← setToList (allReferenceScripts txTop utxo) ] scriptSize x

minfee : PParams → TopLevelTx → UTxO → Coin
minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b
                       + txScriptFee (pp .prices) (totExUnits txTop)
                       + scriptsCost pp (refScriptsSize txTop utxo)


instance
  HasCoin-UTxO : HasCoin UTxO
  HasCoin-UTxO .getCoin = cbalance


data inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Type where
  both   : ∀ {l r}  → l ≤ slot × slot ≤ r  →  inInterval slot (just l   , just r)
  lower  : ∀ {l}    → l ≤ slot             →  inInterval slot (just l   , nothing)
  upper  : ∀ {r}    → slot ≤ r             →  inInterval slot (nothing  , just r)
  none   :                                    inInterval slot (nothing  , nothing)


-- Note: inInterval has to be a type definition for inference to work
instance
  Dec-inInterval : inInterval ⁇²
  Dec-inInterval {slot} {just x  , just y } .dec with x ≤? slot | slot ≤? y
  ... | no ¬p₁ | _      = no λ where (both (h₁ , h₂)) → ¬p₁ h₁
  ... | yes p₁ | no ¬p₂ = no λ where (both (h₁ , h₂)) → ¬p₂ h₂
  ... | yes p₁ | yes p₂ = yes (both (p₁ , p₂))
  Dec-inInterval {slot} {just x  , nothing} .dec with x ≤? slot
  ... | no ¬p = no  (λ where (lower h) → ¬p h)
  ... | yes p = yes (lower p)
  Dec-inInterval {slot} {nothing , just x } .dec with slot ≤? x
  ... | no ¬p = no  (λ where (upper h) → ¬p h)
  ... | yes p = yes (upper p)
  Dec-inInterval {slot} {nothing , nothing} .dec = yes none

coinPolicies : ℙ ScriptHash
coinPolicies = policies (inject 1)

isAdaOnly : Value → Type
isAdaOnly v = policies v ≡ᵉ coinPolicies


collateralCheck : PParams → TopLevelTx → UTxO → Type
collateralCheck pp txTop utxo =
  All (λ (addr , _) → isVKeyAddr addr) (range (utxo ∣ CollateralInputsOf txTop))
  × isAdaOnly (balance (utxo ∣ CollateralInputsOf txTop))
  × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage
  × (CollateralInputsOf txTop) ≢ ∅


module _ (txTop : TopLevelTx) (depositsChange : ℤ) where

  depositRefundsBatch : Coin
  depositRefundsBatch = negPart depositsChange

  newDepositsBatch : Coin
  newDepositsBatch = posPart depositsChange

  consumed : UTxO → Value
  consumed utxo =  consumedTx txTop + inject depositRefundsBatch
                + ∑ˡ[ stx ← SubTransactionsOf txTop ] (consumedTx stx)
    where
    consumedTx : Tx ℓ → Value
    consumedTx tx =  balance (utxo ∣ SpendInputsOf tx)
                     + MintedValueOf tx
                     + inject (getCoin (WithdrawalsOf tx))

  produced : Value
  produced =  producedTx txTop + inject newDepositsBatch
              + ∑ˡ[ stx ← SubTransactionsOf txTop ] (producedTx stx)
    where
    producedTx : ∀ {ℓ} → Tx ℓ → Value
    producedTx {TxLevelSub} tx =  balance (outs tx) + inject (DonationsOf tx)
    producedTx {TxLevelTop} tx =
      balance (outs tx) + inject (TxFeesOf tx) + inject (DonationsOf tx)


private
  variable
    A        : Type
    Γ        : A
    s s'     : UTxOState
    txTop    : TopLevelTx
    txSub    : SubLevelTx


allP2ScriptsWithContext : UTxOEnv → TopLevelTx → List (P2Script × List Data × ExUnits × CostModel)
allP2ScriptsWithContext Γ txTop =
  p2ScriptsWithContext txTop ++ concatMap p2ScriptsWithContext (SubTransactionsOf txTop)
    where
      p2ScriptsWithContext : Tx ℓ → List (P2Script × List Data × ExUnits × CostModel)
      p2ScriptsWithContext t =
        collectP2ScriptsWithContext (PParamsOf Γ)
                                    txTop
                                    (UTxOOf Γ)        -- (1)
                                    (DataPoolOf Γ)    -- (2)
                                    (ScriptPoolOf Γ)  -- (3)


data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → ⊤ → TopLevelTx → ⊤ → Type where

  UTXOS :
    ∙ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop
      ────────────────────────────────
      Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt


private
  variable
    utxo : UTxO
    fees : Fees
    donations : Donations


data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

  SUBUTXO :

    ∙ SpendInputsOf txSub ≢ ∅
    ∙ inInterval (SlotOf Γ) (ValidIntervalOf txSub)
    ∙ MaybeNetworkIdOf txSub ~ just NetworkId
      ────────────────────────────────
    let
         s₁ = if IsTopLevelValidFlagOf Γ
              then $\begin{pmatrix} \,\htmlId{8970}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{8971}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8976}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7179}{\htmlId{8978}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7680}{\htmlId{8992}{\htmlClass{Generalizable}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8998}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{8999}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9001}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4377}{\htmlId{9004}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7680}{\htmlId{9009}{\htmlClass{Generalizable}{\text{txSub}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{9017}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{9024}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9034}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{9036}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7680}{\htmlId{9048}{\htmlClass{Generalizable}{\text{txSub}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{9063}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{9070}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{9077}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$
    in
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{9108}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{9115}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{9122}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ txSub ,SUBUTXO⦈ s₁


unquoteDecl SUBUTXO-premises = genPremises SUBUTXO-premises (quote SUBUTXO)


data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where

  UTXO :

    let
         pp        = PParamsOf Γ
         utxo₀     = UTxOOf Γ
         overhead  = 160
    in
    ∙ SpendInputsOf txTop ≢ ∅
    ∙ inInterval (SlotOf Γ) (ValidIntervalOf txTop)
    ∙ minfee pp txTop utxo ≤ TxFeesOf txTop
    ∙ consumed txTop (DepositsChangeOf Γ) utxo₀ ≡ produced txTop (DepositsChangeOf Γ)
    ∙ SizeOf txTop ≤ maxTxSize pp
    ∙ refScriptsSize txTop utxo₀ ≤ pp .maxRefScriptSizePerTx
    ∙ allSpendInputs txTop ⊆ dom utxo₀                          -- (1)
    ∙ allReferenceInputs txTop ⊆ dom utxo₀                      -- (1)
    ∙ NoOverlappingSpendInputs txTop                            -- (2)
    ∙ requiredGuardsInTopLevel txTop (SubTransactionsOf txTop)  -- (3)
    ∙ RedeemersOf txTop ˢ ≢ ∅ → collateralCheck pp txTop utxo₀
    ∙ allMintedCoin txTop ≡ 0

    ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ]
      (inject ((overhead + utxoEntrySize o) * coinsPerUTxOByte pp) ≤ᵗ txOutToValue o)
      × (serializedSize (txOutToValue o) ≤ maxValSize pp)

    ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ]
      (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ 64)) a × (netId a ≡ NetworkId)

    ∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId
    ∙ MaybeNetworkIdOf txTop ~ just NetworkId
    ∙ CurrentTreasuryOf txTop  ~ just (TreasuryOf Γ)
    ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
      ────────────────────────────────
    let
         s₁ = if IsValidFlagOf txTop then $\begin{pmatrix} \,\htmlId{10709}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{10710}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10715}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7179}{\htmlId{10717}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10731}{\htmlClass{Generalizable}{\text{txTop}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10737}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{10738}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10740}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4377}{\htmlId{10743}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10748}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{10756}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10761}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6240}{\htmlId{10763}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10772}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{10780}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10790}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{10792}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10804}{\htmlClass{Generalizable}{\text{txTop}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{10819}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10824}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\htmlId{10826}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#6075}{\htmlId{10827}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10846}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{10851}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10853}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{10857}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10862}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4514}{\htmlId{10864}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{10873}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{10874}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{10879}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6075}{\htmlId{10881}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7654}{\htmlId{10900}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{10905}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{10909}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$
    in
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Utxo.html#8578}{\htmlId{10940}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8594}{\htmlId{10947}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Utxo.html#8610}{\htmlId{10954}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ txTop ,UTXO⦈ s₁